{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, GADTs,
  FlexibleContexts, UndecidableInstances, ViewPatterns, TemplateHaskell,
  TypeOperators, ScopedTypeVariables, QuasiQuotes #-}

{- |

Module      :  Data.Yoko.Reflect
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

Definitions on top of the basic @yoko@ reflection concepts "Data.Yoko.ReflectBase".

-}

module Data.Yoko.Reflect
  (module Data.Yoko.Reflect, module Data.Yoko.ReflectBase) where

import Type.Yoko

import Data.Yoko.Generic
import Data.Yoko.ReflectBase



{-
type instance Recurs (D a) = V
type instance Recurs (F f c) = Recurs c
type instance Recurs (FF ff c d) =
  NormW (Recurs c) (Recurs d) -- NormW avoiding duplication
type instance Recurs (M i c) = Recurs c
type instance Recurs (N t) = Recurs (Rep t)
type instance Recurs (R t) = N t
type instance Recurs U = V
type instance Recurs V = V
-}




type OnlyDC t = UnN (Fin (DCs t))
type family UnN (u :: * -> *)
type instance UnN ((:=:) dc) = dc

uniqueDC :: (DT t, (:=:) (OnlyDC t) ~ Fin (DCs t), t ~ Range (OnlyDC t)) => t -> RMNI (OnlyDC t)
uniqueDC = uniqueRMN . disband

uniqueRMN :: (Finite u, (:=:) (UnN (Fin u)) ~ Fin u
             ) => AnRMN m u -> RMN m (UnN (Fin u))
uniqueRMN x = case finiteNP x of NP Refl x -> x

uniqueRMN' :: (Finite (DCs (Range dc)), (:=:) dc ~ Fin (DCs (Range dc))
              ) => Disbanded m (Range dc) -> RMN m dc
uniqueRMN' = uniqueRMN




-- @LeftmostRange@ returns the @Range@ of the leftmost type in a type-sum.
type LeftmostRange dcs = Range (Leftmost dcs)
type family Leftmost (u :: * -> *)
type instance Leftmost ((:=:) t) = t
type instance Leftmost (u :|| v) = Leftmost u





data IsDC dc where IsDC :: DC dc => IsDC dc
obvious_membership ''IsDC

newtype RMNTo m b dc = RMNTo {rmnTo :: RMN m dc -> b}; wraps_thinly ''RMNTo




-- | Just a specialization: @dcDispatch = (. disband) . dcDispatch'@.
dcDispatch :: DT t => NT (DCs t) (RMNTo IdM b) -> t -> b
dcDispatch = (. disband) . dcDispatch'

-- | Just a specialization: @dcDispatch' nt ('NP' ('DCOf' tag) fds) = 'appNT'
-- nt tag fds@.
dcDispatch' :: DT t => NT (DCs t) (RMNTo IdM b) -> Disbanded IdM t -> b
dcDispatch' nt (NP tag fds) = appNT nt tag fds




{- | A fundamental notion of identity in @yoko@, the @TagRepIs tag c@ open set
contains all constructor types @dc@ where @(Tag dc ~ tag, c ~ Rep dc)@.

@
  type instance Pred (TagRepIs tag c) dc =
    And (IsEQ (Compare (Tag dc) tag)) (IsEQ (Compare (Rep dc) c))
@

-}
data TagRepIs tag c dc where
  TagRepIs :: (EQ ~ Compare tag tag, EQ ~ Compare c c,
               Tag dc ~ tag, c ~ Rep dc) => TagRepIs tag c dc
obvious_membership_ False True ''TagRepIs

instance (EQ ~ Compare tag tag, EQ ~ Compare c c) => SetModel (TagRepIs tag c) where
  evidence TagRepIs x = x

type instance dc ::? TagRepIs tag c =
  And (IsEQ (Compare (Tag dc) tag)) (IsEQ (Compare (Rep dc) c))

{-data TagGistEQ tag gst m dc where
  TagGistEQ :: (Tag dc ~ tag, Gist (N dc), Gst (N dc) m ~ gst
               ) => TagGistEQ tag gst m dc
obvious_membership ''TagGistEQ
type instance Pred (TagGistEQ tag gst m) dc =
  And (IsEQ (Compare (Tag dc) tag))
      (IsEQ (Compare (Gst (N dc) m) gst))-}





-- | Just a specialization: @bandDCs = band@.
bandDCs :: DT t => Disbanded IdM t -> t; bandDCs = band

fr_DCOf :: forall t dc. DT t => DCs t dc -> RMNI dc -> t
fr_DCOf u = case weakenTo [qP|DCOf t :: * -> *|] u of
  DCOf -> case weaken u of DCSet -> fr
